Nuprl Definition : es-frame 11,40

@i only L affect x:T
== es-dtype(es; i; x; T)
== c alle-at(es; i; e.(((es-kind(es; e)  L))  (es-after(es; x; e) = es-when(es; x; e)))) 
latex



clarification:

es-frame(es;i;L;x;T)
== es-dtype(es; i; x; T)
== c alle-at(es;
== c alle-at(i;
== c alle-at(e.(((es-kind(es; e)  L  Knd))  (es-after(es; x; e) = es-when(es; x; e)  T))
== c alle-at() 
latex


DefinitionsA c B, es-dtype(es; i; x; T), alle-at(es; i; e.P(e)), P  Q, A, (x  l), es-kind(es; e), Knd, s = t, es-after(es; x; e), es-when(es; x; e)
FDL editor aliaseses-frame

origin